Warning: mkdir(): No space left on device in /var/www/tg-me/post.php on line 37

Warning: file_put_contents(aCache/aDaily/post/sqlhub/--): Failed to open stream: No such file or directory in /var/www/tg-me/post.php on line 50
Data Science. SQL hub | Telegram Webview: sqlhub/1867 -
Telegram Group & Telegram Channel
✔️ А вот и новый DeepSeek Prover v2, модель, заточенная исключительно на математику.

🚀Масштабная архитектура на базе, которая содержит 671 млрд параметров, что в 96 раз больше, чем у предыдущей версии Prover-V1.5 (7 млрд).

Построен на базе архитектуры «смеси экспертов» (MoE), что снижает затраты на обучение и повышает эффективность решения задач.

Модель заточена на формальное доказательство теорем с помощью языка программирования Lean 4, обеспечивая 100% логическую точность.

Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем.

Результаты:
Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.

Для тренировки использовались 8 млн синтетических примеров, созданных через рекурсивный поиск решений теорем.

🔍 Как это работает:

1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.

2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.

3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.

🌟 Два размера:
7 B — базовый вариант.
671 B — расширенная версия на базе DeepSeek-V3-Base.

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
Please open Telegram to view this post
VIEW IN TELEGRAM



tg-me.com/sqlhub/1867
Create:
Last Update:

✔️ А вот и новый DeepSeek Prover v2, модель, заточенная исключительно на математику.

🚀Масштабная архитектура на базе, которая содержит 671 млрд параметров, что в 96 раз больше, чем у предыдущей версии Prover-V1.5 (7 млрд).

Построен на базе архитектуры «смеси экспертов» (MoE), что снижает затраты на обучение и повышает эффективность решения задач.

Модель заточена на формальное доказательство теорем с помощью языка программирования Lean 4, обеспечивая 100% логическую точность.

Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем.

Результаты:
Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.

Для тренировки использовались 8 млн синтетических примеров, созданных через рекурсивный поиск решений теорем.

🔍 Как это работает:

1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.

2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.

3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.

🌟 Два размера:
7 B — базовый вариант.
671 B — расширенная версия на базе DeepSeek-V3-Base.

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

BY Data Science. SQL hub




Share with your friend now:
tg-me.com/sqlhub/1867

View MORE
Open in Telegram


Data Science SQL hub Telegram | DID YOU KNOW?

Date: |

Among the actives, Ascendas REIT sank 0.64 percent, while CapitaLand Integrated Commercial Trust plummeted 1.42 percent, City Developments plunged 1.12 percent, Dairy Farm International tumbled 0.86 percent, DBS Group skidded 0.68 percent, Genting Singapore retreated 0.67 percent, Hongkong Land climbed 1.30 percent, Mapletree Commercial Trust lost 0.47 percent, Mapletree Logistics Trust tanked 0.95 percent, Oversea-Chinese Banking Corporation dropped 0.61 percent, SATS rose 0.24 percent, SembCorp Industries shed 0.54 percent, Singapore Airlines surrendered 0.79 percent, Singapore Exchange slid 0.30 percent, Singapore Press Holdings declined 1.03 percent, Singapore Technologies Engineering dipped 0.26 percent, SingTel advanced 0.81 percent, United Overseas Bank fell 0.39 percent, Wilmar International eased 0.24 percent, Yangzijiang Shipbuilding jumped 1.42 percent and Keppel Corp, Thai Beverage, CapitaLand and Comfort DelGro were unchanged.

For some time, Mr. Durov and a few dozen staffers had no fixed headquarters, but rather traveled the world, setting up shop in one city after another, he told the Journal in 2016. The company now has its operational base in Dubai, though it says it doesn’t keep servers there.Mr. Durov maintains a yearslong friendship from his VK days with actor and tech investor Jared Leto, with whom he shares an ascetic lifestyle that eschews meat and alcohol.

Data Science SQL hub from tr


Telegram Data Science. SQL hub
FROM USA